Nuprl Lemma : f2f+-p+-total 11,40

es:ES, ff:FIFO, f2f+:F2F+-decls.
plus-ify{i:l}(es;ff;is_req  ;is_ack ;awaiting ;owes_ack )
 (sndrrcvr:ff.C, ee':E.
 ([esndr is_req   rcvr [ercvr is_ack  sndr])
  ([e'sndr is_req   rcvr [e'rcvr is_ack  sndr])
  (((f2f+-p+(e,e'))  (e = e'))  (f2f+-p+(e',e)))) 
latex


Definitionsx(s), A c B, , t  T, P & Q, P  Q, P  Q, x:AB(x), x f y, {T}, f2f+-p+
Lemmasf2f+-pred-field, f2f+-pred wf, generated-thread-properties2, f2f+-pred-generates-thread, event system wf, FIFO wf, F2F+-decls wf, fifoS wf, fifoR wf, f2f+Owes wf, f2f+Wait wf, plus-ify wf, fifoC wf, es-E wf, f2f+Ack wf, f2f+Req wf, snd-it wf, f2f+-property

origin